0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 19 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 1 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
append3C_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appendA_in_gga(T18, T11, T13))
appendA_in_gga([], T25, T25) → appendA_out_gga([], T25, T25)
appendA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appendA_out_gga(T35, T36, T38)) → appendA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appendA_out_gga(T18, T11, T13)) → append3C_out_ggga([], T18, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
appendB_in_gga([], T59, T59) → appendB_out_gga([], T59, T59)
appendB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appendB_out_gga(T67, T68, X74)) → appendB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, X50)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appendA_out_gga(.(T47, T52), T11, T13)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
append3C_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appendA_in_gga(T18, T11, T13))
appendA_in_gga([], T25, T25) → appendA_out_gga([], T25, T25)
appendA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appendA_out_gga(T35, T36, T38)) → appendA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appendA_out_gga(T18, T11, T13)) → append3C_out_ggga([], T18, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
appendB_in_gga([], T59, T59) → appendB_out_gga([], T59, T59)
appendB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appendB_out_gga(T67, T68, X74)) → appendB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, X50)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appendA_out_gga(.(T47, T52), T11, T13)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
APPEND3C_IN_GGGA([], T18, T11, T13) → U3_GGGA(T18, T11, T13, appendA_in_gga(T18, T11, T13))
APPEND3C_IN_GGGA([], T18, T11, T13) → APPENDA_IN_GGA(T18, T11, T13)
APPENDA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U1_GGA(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
APPENDA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDA_IN_GGA(T35, T36, T38)
APPEND3C_IN_GGGA(.(T47, T48), T49, T11, T13) → U4_GGGA(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
APPEND3C_IN_GGGA(.(T47, T48), T49, T11, T13) → APPENDB_IN_GGA(T48, T49, X50)
APPENDB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U2_GGA(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
APPENDB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDB_IN_GGA(T67, T68, X74)
APPEND3C_IN_GGGA(.(T47, T48), T49, T11, T13) → U5_GGGA(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_GGGA(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_GGGA(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U5_GGGA(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → APPENDA_IN_GGA(.(T47, T52), T11, T13)
append3C_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appendA_in_gga(T18, T11, T13))
appendA_in_gga([], T25, T25) → appendA_out_gga([], T25, T25)
appendA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appendA_out_gga(T35, T36, T38)) → appendA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appendA_out_gga(T18, T11, T13)) → append3C_out_ggga([], T18, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
appendB_in_gga([], T59, T59) → appendB_out_gga([], T59, T59)
appendB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appendB_out_gga(T67, T68, X74)) → appendB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, X50)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appendA_out_gga(.(T47, T52), T11, T13)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
APPEND3C_IN_GGGA([], T18, T11, T13) → U3_GGGA(T18, T11, T13, appendA_in_gga(T18, T11, T13))
APPEND3C_IN_GGGA([], T18, T11, T13) → APPENDA_IN_GGA(T18, T11, T13)
APPENDA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U1_GGA(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
APPENDA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDA_IN_GGA(T35, T36, T38)
APPEND3C_IN_GGGA(.(T47, T48), T49, T11, T13) → U4_GGGA(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
APPEND3C_IN_GGGA(.(T47, T48), T49, T11, T13) → APPENDB_IN_GGA(T48, T49, X50)
APPENDB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U2_GGA(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
APPENDB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDB_IN_GGA(T67, T68, X74)
APPEND3C_IN_GGGA(.(T47, T48), T49, T11, T13) → U5_GGGA(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_GGGA(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_GGGA(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U5_GGGA(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → APPENDA_IN_GGA(.(T47, T52), T11, T13)
append3C_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appendA_in_gga(T18, T11, T13))
appendA_in_gga([], T25, T25) → appendA_out_gga([], T25, T25)
appendA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appendA_out_gga(T35, T36, T38)) → appendA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appendA_out_gga(T18, T11, T13)) → append3C_out_ggga([], T18, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
appendB_in_gga([], T59, T59) → appendB_out_gga([], T59, T59)
appendB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appendB_out_gga(T67, T68, X74)) → appendB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, X50)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appendA_out_gga(.(T47, T52), T11, T13)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
APPENDB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDB_IN_GGA(T67, T68, X74)
append3C_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appendA_in_gga(T18, T11, T13))
appendA_in_gga([], T25, T25) → appendA_out_gga([], T25, T25)
appendA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appendA_out_gga(T35, T36, T38)) → appendA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appendA_out_gga(T18, T11, T13)) → append3C_out_ggga([], T18, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
appendB_in_gga([], T59, T59) → appendB_out_gga([], T59, T59)
appendB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appendB_out_gga(T67, T68, X74)) → appendB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, X50)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appendA_out_gga(.(T47, T52), T11, T13)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
APPENDB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPENDB_IN_GGA(T67, T68, X74)
APPENDB_IN_GGA(.(T66, T67), T68) → APPENDB_IN_GGA(T67, T68)
From the DPs we obtained the following set of size-change graphs:
APPENDA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDA_IN_GGA(T35, T36, T38)
append3C_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appendA_in_gga(T18, T11, T13))
appendA_in_gga([], T25, T25) → appendA_out_gga([], T25, T25)
appendA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appendA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appendA_out_gga(T35, T36, T38)) → appendA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appendA_out_gga(T18, T11, T13)) → append3C_out_ggga([], T18, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, X50))
appendB_in_gga([], T59, T59) → appendB_out_gga([], T59, T59)
appendB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appendB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appendB_out_gga(T67, T68, X74)) → appendB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, X50)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
append3C_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appendB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appendB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appendA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appendA_out_gga(.(T47, T52), T11, T13)) → append3C_out_ggga(.(T47, T48), T49, T11, T13)
APPENDA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPENDA_IN_GGA(T35, T36, T38)
APPENDA_IN_GGA(.(T34, T35), T36) → APPENDA_IN_GGA(T35, T36)
From the DPs we obtained the following set of size-change graphs: